\begin{tabbing}
$\forall$$D$:Dsys.
\\[0ex]Feasible($D$)
\\[0ex]$\Rightarrow$ (\=$\forall$$i$:Id, $l$:IdLnk, ${\it tg}$:Id.\+
\\[0ex]if destination($l$) = $i$$\rightarrow$ M(source($l$)).dout($l$,${\it tg}$) else Void fi $\subseteq\rho$ M($i$).da(rcv($l$,${\it tg}$)))
\-
\end{tabbing}